COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1200}
C00007 ENDMK
C⊗;
\magnify{1200}
\output{\shipout\box255}
\def\xskip{\hskip7pt plus3pt minus4pt}
\chcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 4pt

\ctrline{\bf CS 206---Recursive Programming and Proving}
\vskip 20pt
\ctrline{Homework 3}
\ctrline{Due Thursday, November 4, 1982}
\vskip 10pt

Do problems 1 and 2 on page 89 of {\sl LISP: Programming and Proving}.
Problem 1 uses functions that you have already written and run on the
computer.  Problem 2 uses functions defined on pages 46--47, which
you should write and hand in along with the proofs.  You are not
required to test them on the computer, but doing so may help you convince
yourself that they are correct before you prove things about them.

\vskip 20pt
\ctrline{Homework 4}
\ctrline{Due Thursday, November 11, 1982}
\vskip 10pt

Write functions to do the following, and debug and run them on the computer.

\item{(1)} The function |convert| takes a list, which we interpret as a
LISP functional form (i.e., the |car| is a function and the |cdr| is a
list of arguments), and performs indicated $λ$-conversions.  For example,
on the input {\tt ((LAMBDA (X) (CONS X Y)) (CAR Z))}, the returned value
should be {\tt (CONS (CAR Z) Y)}.  There may be nested $λ$-conversions, so
for example the input
$$\vbox{\hbox{\tt ((LAMBDA (APPLE PEAR) (ORANGE PEAR APPLE))}
	\hbox{\tt\ GRAPE ((LAMBDA (PLUM) (GRAPE PLUM)) LIME))}}$$
should return {\tt (ORANGE (GRAPE LIME) GRAPE)}.

\item{(2)} The function |uncommon| removes common subexpressions from
lists of the same form.  This is essentially the inverse of the function
|convert|.  For example, |uncommon| on input {\tt (CONS (CAR X) (CAR X))}
will return {\tt ((LAMBDA (G0001) (CONS G0001 G0001)) (CAR X))}.  The
way that you create new symbols, like {\tt G0001}, in MacLisp
is to call the function {\tt (GENSYM)}, which returns a different atom
each time it is called.

\hangindent 20pt after 0
There is some question about what should be recognized as common
subexpressions.  Certainly if $|equal|[x,y]$ you should recognize $x$ and
$y$ as the same.\xskip (Unless they contain different {\tt LAMBDA}-bound
variables of the same name.)\xskip  Anything else may be considered
extra credit.  Two cases you might work on are:
\itemitem{(a)} Expressions like {\tt (CAR (CDR X))} are the same as
{\tt (CADR X)}.
\itemitem{(b)} Expressions are the same when they differ only in the
names of {\tt LAMBDA}-bound variables, e.g., {\tt (LAMBDA (X) (F X Y))}
and {\tt (LAMBDA (Z) (F Z Y))}.

Neither of these programs can be guaranteed to terminate; consider what
they will do on the input {\tt ((LAMBDA (X) (X X)) (LAMBDA (X) (X X)))}.
Unless you make this a special case, program (1) will run forever, and
program (2) will if you have implemented part (b).  This example does
depend on the fact that you can apply a {\tt LAMBDA}-variable as a
function, which is not a part of ``first-order'' LISP.

\vfill\end